i, a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp),
init:{f:x:Id fp ds(x)?Top| x:Id. x  dom(ds)  x  dom(f) }, es:ES.
pre-init-p2(es;i;ds;init;a;T;P)  Prop 

latex

Definitions	x:A. B(x), Prop, f(x)?z, P  Q, t  T, pre-init-p2(es;i;ds;init;a;T;P), P & Q, x. t(x), if b t else f fi, true, false, , x(s), Unit, P  Q, A, False,
Lemmas	pre-init-p wf, pre-p wf, Id wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, init-p wf, fpf-ap wf, fpf-cap wf, top wf, bool wf, eqtt to assert, subtype rel self, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, event system wf, fpf wf, decl-state wf